\begin{tabbing}
$\forall$$A$:es\_realizer\{i:l\}, $P$,$Q$:(event\_system\{i:l\}$\rightarrow$prop\{i':l\}).
\\[0ex]R{-}realizes\=\{i:l\}\+
\\[0ex]($A$; ${\it es}$.$P$(${\it es}$))
\-\\[0ex]$\Rightarrow$ ($\forall$${\it es}$:event\_system\{i:l\}. $P$(${\it es}$) $\Rightarrow$ $Q$(${\it es}$))
\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex]($A$; ${\it es}$.$Q$(${\it es}$))
\-
\end{tabbing}